Nuprl Lemma : proper_sublist_length
11,40
postcript
pdf
T
:Type,
L1
,
L2
:(
T
List).
L1
L2
(||
L1
|| = ||
L2
||
)
(
L1
=
L2
)
latex
Definitions
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
i
j
<
k
,
P
&
Q
,
{
i
..
j
}
,
suptype(
S
;
T
)
,
S
T
,
False
,
A
,
A
B
,
,
{
T
}
,
SQType(
T
)
,
x
:
A
.
B
(
x
)
,
L1
L2
Lemmas
sublist
wf
,
length
wf1
,
nat
wf
,
list
extensionality
,
le
wf
,
int
seg
wf
,
increasing
is
id
origin
T:Type, L1, L2:(T List). L1 
L2 
(||L1|| = ||L2|| 
) (L1 = L2) T:Type, L1, L2:(T List). L1 L2 (||L1|| = ||L2|| ) (L1 = L2) 
T Qx:A. B(x)
j < k
} T
A B
x:A. B(x) L2